T:Type, as, cs, bs, ds:T List. as @ bs || cs @ ds  as || cs 

latex

Definitions	t  T, l1 || l2, P  Q, x:A. B(x), l1  l2, P  Q, as @ bs, {T}, P & Q, P  Q, P  Q
Lemmas	compat-cons, nil iseg, compat wf, append wf, iseg wf